z:. (z = 0  ) 

latex

Definitions	, t  T, True, (i = j), tt, if b then t else f fi , qeq(r;s), b, False, P  Q, A, x:A. B(x), a  b  T , P & Q, P  Q,
Lemmas	int nzero wf, int-rational, assert of eq int, qeq wf2, assert wf